D:Dsys, i:Id, k:Knd. Feasible(D)  AtomFree(Type;d-decl(D;i)(k)) 

latex

Definitions	P  Q, AtomFree(T;x), Type, Feasible(D), x:A. B(x), Id, t  T, Dsys, Knd, left+right, x:AB(x), d-decl(D;i), w-action-dec(TA;M;i), kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), Unit, P  Q, P & Q, x:AB(x), a = b, , b, A, b, Prop, s = t, destination(l), Void, Feasible(M), M(i), source(l), locl(a)
Lemmas	locl wf, ma-da-atom-free, lsrc wf, d-m wf, ma-dout-atom-free, ldst wf, assert wf, not wf, bnot wf, bool wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, dsys wf, Id wf, Knd wf, d-feasible wf